T:Type, L:T List, R:({x:T| (x  L) }Realizer), A:Realizer.
A || xL.R(x)  (x:T. (x  L)  A || R(x)) 

latex

Definitions	x:A. B(x), t  T, P  Q, x(s), P  Q, Top, x. t(x), P & Q, P  Q, Prop, P  Q, {T}, l[i], {i..j}, ||as||, Y, i  j < k, hd(l), nth_tl(n;as), if b t else f fi, ij, b, i<j, true, false, (x  l), A & B, x:A. B(x), AB, A, False,
Lemmas	Rall-nil, l member wf, R-compat wf, Rnone wf, es realizer wf, nil member, R-compat-symmetry, R-compat-none, subtype rel function, cons member, subtype rel self, Rall-cons, select member, length wf1, non neg length, iff functionality wrt iff, Rplus wf, Rall wf, R-compat-Rplus2, nat wf, select wf, and functionality wrt iff